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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl2  1211  simpl2l  1245  simpl2r  1246  simpl21  1270  simpl22  1271  simpl23  1272  fcofo  7298  cocan1  7301  onelfvnef1  8454  curfv  8897  ordiso2  9514  fin1a2lem9  10491  fin1a2lem12  10494  gchpwdom  10760  winainflem  10783  bpolydif  16228  dvdsmodexp  16437  muldvds1  16457  lcmdvds  16790  ramcl  17214  oddvdsnn0  19765  ghmplusg  20067  frlmsslss2  22088  frlmsslsp  22109  islindf4  22151  mamures  22719  matepmcl  22784  matepm2cl  22785  pmatcollpw2lem  23102  cnpnei  23589  ssref  23838  qtopss  24041  elfm2  24274  flffbas  24321  cnpfcf  24367  deg1ldg  26417  brbtwn2  29490  colinearalg  29495  axsegconlem1  29502  upgrpredgv  29724  cusgrrusgr  30169  upgrewlkle2  30194  wwlksm1edg  30477  clwwlkf  30645  wwlksext2clwwlk  30655  nvmul0or  31259  hoadddi  32412  volfiniune  34911  bnj548  35575  funsseq  36627  nn0prpwlem  37204  fnemeet1  37248  lindsadd  38643  keridl  39073  pmapglbx  40933  elpaddn0  40964  paddasslem9  40992  paddasslem10  40993  cdleme42mgN  41652  relexpxpmin  44824  ntrclsk3  45177  n0p  46169  wessf1ornlem  46307  infxr  46485  lptre2pt  46757  dvnprodlem1  47063  fourierdlem42  47266  fourierdlem48  47271  fourierdlem54  47277  fourierdlem77  47300  sge0rpcpnf  47538  hoicvr  47665  smflimsuplem7  47943