Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3adant3r1 | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.) |
Ref | Expression |
---|---|
ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant3r1 | ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad4ant3.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3expb 1122 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | 3adantr1 1171 | 1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: ccatswrd 14230 plttr 17845 pltletr 17846 latjlej1 17956 latjlej2 17957 latnlej 17959 latnlej2 17962 latmlem2 17973 latledi 17980 latjass 17986 latj32 17988 latj13 17989 ipopos 18039 tsrlemax 18089 imasmnd2 18207 grpsubsub 18449 grpnnncan2 18457 imasgrp2 18475 mulgnn0ass 18524 mulgsubdir 18528 cmn32 19186 ablsubadd 19194 imasring 19634 zntoslem 20518 xmettri3 23248 mettri3 23249 xmetrtri 23250 xmetrtri2 23251 metrtri 23252 cphdivcl 24076 cphassr 24106 relogbmulexp 25658 grpodivdiv 28618 grpomuldivass 28619 ablo32 28627 ablodivdiv4 28632 ablodiv32 28633 nvmdi 28726 dipdi 28921 dipassr 28924 dipsubdir 28926 dipsubdi 28927 dvrcan5 31206 cgr3tr4 34088 cgr3rflx 34090 endofsegid 34121 seglemin 34149 broutsideof2 34158 rngosubdi 35838 rngosubdir 35839 isdrngo2 35851 crngm23 35895 dmncan2 35970 latmassOLD 36978 latm32 36980 cvrnbtwn4 37028 cvrcmp2 37033 ltcvrntr 37173 atcvrj0 37177 3dim3 37218 paddasslem17 37585 paddass 37587 lautlt 37840 lautcvr 37841 lautj 37842 lautm 37843 erngdvlem3 38739 dvalveclem 38774 isdomn4 39892 mendlmod 40719 |
Copyright terms: Public domain | W3C validator |