Theorem 3ad2antl2 1205

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 727	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1185	1 ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  simpl2  1211  simpl2l  1245  simpl2r  1246  simpl21  1270  simpl22  1271  simpl23  1272  fcofo  7286  cocan1  7289  ordiso2  9473  fin1a2lem9  10387  fin1a2lem12  10390  gchpwdom  10650  winainflem  10673  bpolydif  16104  dvdsmodexp  16313  muldvds1  16333  lcmdvds  16661  ramcl  17084  oddvdsnn0  19609  ghmplusg  19911  frlmsslss2  21925  frlmsslsp  21946  islindf4  21988  mamures  22554  matepmcl  22619  matepm2cl  22620  pmatcollpw2lem  22934  cnpnei  23421  ssref  23669  qtopss  23872  elfm2  24105  flffbas  24152  cnpfcf  24198  deg1ldg  26249  brbtwn2  29255  colinearalg  29260  axsegconlem1  29267  upgrpredgv  29489  cusgrrusgr  29931  upgrewlkle2  29956  wwlksm1edg  30230  clwwlkf  30398  wwlksext2clwwlk  30408  nvmul0or  31002  hoadddi  32155  volfiniune  34620  bnj548  35285  funsseq  36260  nn0prpwlem  36833  fnemeet1  36877  curfv  38251  lindsadd  38264  keridl  38683  pmapglbx  40543  elpaddn0  40574  paddasslem9  40602  paddasslem10  40603  cdleme42mgN  41262  relexpxpmin  44443  ntrclsk3  44796  n0p  45765  wessf1ornlem  45903  infxr  46082  lptre2pt  46354  dvnprodlem1  46660  fourierdlem42  46863  fourierdlem48  46868  fourierdlem54  46874  fourierdlem77  46897  sge0rpcpnf  47135  hoicvr  47262  smflimsuplem7  47540