![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adant3r2 | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.) |
Ref | Expression |
---|---|
ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant3r2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad4ant3.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3expb 1100 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | 3adantr2 1150 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 |
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 199 df-an 388 df-3an 1070 |
This theorem is referenced by: plttr 17432 latjlej2 17528 latmlem1 17543 latmlem2 17544 latledi 17551 latmlej11 17552 latmlej12 17553 ipopos 17622 grppnpcan2 17974 mulgsubdir 18045 imasring 19086 zntoslem 20399 mettri2 22648 mettri 22659 xmetrtri 22662 xmetrtri2 22663 metrtri 22664 ablomuldiv 28100 ablonnncan1 28105 nvmdi 28196 dipdi 28391 dipassr 28394 dipsubdir 28396 dipsubdi 28397 btwncomim 32995 cgr3tr4 33034 cgr3rflx 33036 colinbtwnle 33100 rngosubdi 34665 rngosubdir 34666 dmncan1 34796 dmncan2 34797 omlfh1N 35839 omlfh3N 35840 cvrnbtwn3 35857 cvrnbtwn4 35860 cvrcmp2 35865 hlatjrot 35954 cvrat3 36023 lplnribN 36132 ltrn2ateq 36761 dvalveclem 37606 mendlmod 39189 |
Copyright terms: Public domain | W3C validator |