Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3adantl3 | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
Ref | Expression |
---|---|
3adantl.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adantl3 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpa 1058 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜏) → (𝜑 ∧ 𝜓)) | |
2 | 3adantl.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylan 488 | 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: dif1en 8193 infpssrlem4 9128 fin23lem11 9139 tskwun 9606 gruf 9633 lediv2a 10917 prunioo 12301 nn0p1elfzo 12510 rpnnen2lem7 14949 muldvds1 15006 muldvds2 15007 dvdscmul 15008 dvdsmulc 15009 rpexp 15432 pospropd 17134 mdetmul 20429 elcls 20877 iscnp4 21067 cnpnei 21068 cnpflf2 21804 cnpflf 21805 cnpfcf 21845 xbln0 22219 blcls 22311 iimulcl 22736 icccvx 22749 iscau2 23075 rrxcph 23180 cncombf 23425 mumul 24907 ax5seglem1 25808 ax5seglem2 25809 clwwlkinwwlk 26905 wwlksext2clwwlk 26924 nvmul0or 27505 fh1 28477 fh2 28478 cm2j 28479 pjoi0 28576 hoadddi 28662 hmopco 28882 padct 29497 iocinif 29543 volfiniune 30293 eulerpartlemb 30430 ivthALT 32330 cnambfre 33458 rngohomco 33773 rngoisoco 33781 pexmidlem3N 35258 hdmapglem7 37221 relexpmulg 38002 supxrgere 39549 supxrgelem 39553 supxrge 39554 infxr 39583 infleinflem2 39587 rexabslelem 39645 lptre2pt 39872 fnlimfvre 39906 limsupmnfuzlem 39958 climisp 39978 limsupgtlem 40009 dvnprodlem1 40161 ibliccsinexp 40166 iblioosinexp 40168 fourierdlem12 40336 fourierdlem41 40365 fourierdlem42 40366 fourierdlem48 40371 fourierdlem49 40372 fourierdlem51 40374 fourierdlem73 40396 fourierdlem74 40397 fourierdlem75 40398 fourierdlem97 40420 etransclem24 40475 ioorrnopnlem 40524 issalnnd 40563 sge0rpcpnf 40638 sge0seq 40663 smfmullem4 41001 smflimsupmpt 41035 smfliminfmpt 41038 lincdifsn 42213 |
Copyright terms: Public domain | W3C validator |