Theorem 3ad2antl2 1243

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113

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 387  df-3an 1115

This theorem is referenced by:  simpl2  1250  simpl2l  1303  simpl2r  1305  simpl21  1341  simpl22  1343  simpl23  1345  fcofo  6798  cocan1  6801  ordiso2  8689  fin1a2lem9  9545  fin1a2lem12  9548  gchpwdom  9807  winainflem  9830  bpolydif  15158  dvdsmodexp  15365  muldvds1  15383  lcmdvds  15694  ramcl  16104  gsumccat  17731  oddvdsnn0  18314  ghmplusg  18602  frlmsslss2  20481  frlmsslsp  20502  islindf4  20544  mamures  20563  matepmcl  20636  matepm2cl  20637  pmatcollpw2lem  20952  cnpnei  21439  ssref  21686  qtopss  21889  elfm2  22122  flffbas  22169  cnpfcf  22215  deg1ldg  24251  brbtwn2  26204  colinearalg  26209  axsegconlem1  26216  upgrpredgv  26438  cusgrrusgr  26879  upgrewlkle2  26904  wwlksm1edg  27180  wwlksm1edgOLD  27181  clwwlkfOLD  27392  clwwlkf  27397  wwlksext2clwwlk  27409  nvmul0or  28060  hoadddi  29217  volfiniune  30838  bnj548  31513  funsseq  32208  nn0prpwlem  32855  fnemeet1  32899  curfv  33932  lindsadd  33946  keridl  34373  pmapglbx  35844  elpaddn0  35875  paddasslem9  35903  paddasslem10  35904  cdleme42mgN  36563  relexpxpmin  38850  ntrclsk3  39208  n0p  40026  wessf1ornlem  40179  infxr  40380  lptre2pt  40667  dvnprodlem1  40956  fourierdlem42  41160  fourierdlem48  41165  fourierdlem54  41171  fourierdlem77  41194  sge0rpcpnf  41429  hoicvr  41556  smflimsuplem7  41826  isomgrsym  42554