New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3ad2ant3 | Unicode version |
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
Ref | Expression |
---|---|
3ad2ant.1 |
Ref | Expression |
---|---|
3ad2ant3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ad2ant.1 | . . 3 | |
2 | 1 | adantl 452 | . 2 |
3 | 2 | 3adant1 973 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 w3a 934 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-an 360 df-3an 936 |
This theorem is referenced by: simp3l 983 simp3r 984 simp31 991 simp32 992 simp33 993 simp3ll 1026 simp3lr 1027 simp3rl 1028 simp3rr 1029 simp3l1 1060 simp3l2 1061 simp3l3 1062 simp3r1 1063 simp3r2 1064 simp3r3 1065 simp31l 1078 simp31r 1079 simp32l 1080 simp32r 1081 simp33l 1082 simp33r 1083 simp311 1102 simp312 1103 simp313 1104 simp321 1105 simp322 1106 simp323 1107 simp331 1108 simp332 1109 simp333 1110 3anim123i 1137 3jaao 1249 ceqsalt 2881 ceqsralt 2882 vtoclgft 2905 nnsucelrlem3 4426 nnsucelr 4428 ltfintri 4466 ssfin 4470 tfin11 4493 tfinltfinlem1 4500 sfintfin 4532 sfin111 4536 funprg 5149 fnprg 5153 fvun1 5379 ider 5943 ssetpov 5944 eqer 5961 elmapg 6012 elpmg 6013 ener 6039 enadj 6060 enprmaplem6 6081 nenpw1pwlem2 6085 elce 6175 addlec 6208 lenc 6223 taddc 6229 |
Copyright terms: Public domain | W3C validator |