Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3adant3r2 | Structured version Visualization version Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3adant3r2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 | |
2 | 1 | 3expb 1266 | . 2 |
3 | 2 | 3adantr2 1221 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 386 df-3an 1039 |
This theorem is referenced by: plttr 16970 latjlej2 17066 latmlem1 17081 latmlem2 17082 latledi 17089 latmlej11 17090 latmlej12 17091 ipopos 17160 grppnpcan2 17509 mulgsubdir 17582 imasring 18619 zntoslem 19905 mettri2 22146 mettri 22157 xmetrtri 22160 xmetrtri2 22161 metrtri 22162 ablomuldiv 27406 ablonnncan1 27412 nvmdi 27503 dipdi 27698 dipassr 27701 dipsubdir 27703 dipsubdi 27704 btwncomim 32120 cgr3tr4 32159 cgr3rflx 32161 colinbtwnle 32225 rngosubdi 33744 rngosubdir 33745 dmncan1 33875 dmncan2 33876 omlfh1N 34545 omlfh3N 34546 cvrnbtwn3 34563 cvrnbtwn4 34566 cvrcmp2 34571 hlatjrot 34659 cvrat3 34728 lplnribN 34837 ltrn2ateq 35467 dvalveclem 36314 mendlmod 37763 |
Copyright terms: Public domain | W3C validator |