Theorem 3ad2antl2 1217

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antl2	⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3ad2antl2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantlr 747	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1210	1 ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  fcofo  6443  cocan1  6446  ordiso2  8303  fin1a2lem9  9113  fin1a2lem12  9116  gchpwdom  9371  winainflem  9394  bpolydif  14625  muldvds1  14844  lcmdvds  15159  ramcl  15571  gsumccat  17201  oddvdsnn0  17786  ghmplusg  18072  frlmsslss2  19933  frlmsslsp  19954  islindf4  19996  mamures  20015  matepmcl  20087  matepm2cl  20088  pmatcollpw2lem  20401  cnpnei  20878  ssref  21125  qtopss  21328  elfm2  21562  flffbas  21609  cnpfcf  21655  deg1ldg  23656  brbtwn2  25585  colinearalg  25590  axsegconlem1  25597  clwwlkf  26322  2spontn0vne  26414  usgreghash2spot  26596  nvmul0or  26889  hoadddi  28046  volfiniune  29620  bnj548  30221  funsseq  30912  nn0prpwlem  31487  fnemeet1  31531  curfv  32559  keridl  33001  pmapglbx  34073  elpaddn0  34104  paddasslem9  34132  paddasslem10  34133  cdleme42mgN  34794  relexpxpmin  37028  ntrclsk3  37388  n0p  38234  wessf1ornlem  38366  infxr  38524  lptre2pt  38707  dvnprodlem1  38836  fourierdlem42  39042  fourierdlem48  39047  fourierdlem54  39053  fourierdlem77  39076  sge0rpcpnf  39314  hoicvr  39438  cusgrrusgr  40781  upgrewlkle2  40808  wwlksm1edg  41078  clwwlksf  41222