![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3ad2ant2 | GIF version |
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
Ref | Expression |
---|---|
3ad2ant.1 | ⊢ (φ → χ) |
Ref | Expression |
---|---|
3ad2ant2 | ⊢ ((ψ ∧ φ ∧ θ) → χ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ad2ant.1 | . . 3 ⊢ (φ → χ) | |
2 | 1 | adantr 261 | . 2 ⊢ ((φ ∧ θ) → χ) |
3 | 2 | 3adant1 921 | 1 ⊢ ((ψ ∧ φ ∧ θ) → χ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 884 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 886 |
This theorem is referenced by: simp2l 929 simp2r 930 simp21 936 simp22 937 simp23 938 simp2ll 970 simp2lr 971 simp2rl 972 simp2rr 973 simp2l1 1002 simp2l2 1003 simp2l3 1004 simp2r1 1005 simp2r2 1006 simp2r3 1007 simp21l 1020 simp21r 1021 simp22l 1022 simp22r 1023 simp23l 1024 simp23r 1025 simp211 1041 simp212 1042 simp213 1043 simp221 1044 simp222 1045 simp223 1046 simp231 1047 simp232 1048 simp233 1049 3anim123i 1088 3jaao 1202 ceqsalt 2574 vtoclgft 2598 vtoclegft 2619 elirr 4224 en2lp 4232 sotri3 4666 funtpg 4893 fnprg 4897 fntpg 4898 funimaexglem 4925 fnco 4950 fvun1 5182 oprssov 5584 caovimo 5636 rdgivallem 5908 f1dom2g 6172 distrnqg 6371 distrnq0 6442 prarloclem5 6483 cauappcvgprlemlol 6619 cauappcvgprlemupu 6621 caucvgprlemlol 6641 caucvgprlemupu 6643 cnegexlem2 6984 apcotr 7391 apadd1 7392 mulext1 7396 div2negap 7493 ltdiv2 7634 nndivtr 7736 zdivmul 8106 gtndiv 8111 fzind 8129 eluzuzle 8257 eluzp1p1 8274 peano2uz 8302 qdivcl 8352 irrmul 8356 xrre2 8504 ubioc1 8568 ubicc2 8623 uzsubsubfz 8681 elfz1b 8722 fzp1nel 8736 fz0fzdiffz0 8757 difelfzle 8762 elfzo0 8808 elfzonlteqm1 8836 fzonn0p1p1 8839 fzosplitprm1 8860 fzoshftral 8864 expival 8911 redivap 9102 imdivap 9109 |
Copyright terms: Public domain | W3C validator |