Theorem ad3antlr 493

Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem ad3antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ad2antlr 489	. 2 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)
3	2	adantr 276	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad4antlr  495  nntr2  6499  phpm  6860  phplem4on  6862  fidifsnen  6865  fisbth  6878  fin0  6880  fin0or  6881  fiintim  6923  fisseneq  6926  djudom  7087  difinfsnlem  7093  nnnninfeq  7121  nnnninfeq2  7122  enomnilem  7131  enmkvlem  7154  enwomnilem  7162  exmidapne  7254  prmuloc  7560  cauappcvgprlemopl  7640  cauappcvgprlemdisj  7645  cauappcvgprlemladdfl  7649  caucvgprlemopl  7663  axcaucvglemcau  7892  xnn0letri  9797  xaddf  9838  xleaddadd  9881  ssfzo12bi  10218  rebtwn2zlemstep  10246  btwnzge0  10293  addmodlteq  10391  frecuzrdgg  10409  qsqeqor  10623  apexp1  10689  hashxp  10797  cjap  10906  caucvgre  10981  minmax  11229  xrminmax  11264  sumeq2  11358  fsumconst  11453  ntrivcvgap  11547  prodeq2  11556  p1modz1  11792  bezoutlemmain  11989  dfgcd2  12005  uzwodc  12028  lcmgcdlem  12067  mulgval  12914  cnpnei  13501  cnntr  13507  txmetcnp  13800  lgsval  14187  pw1nct  14523  peano4nninf  14526