ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantllr GIF version

Theorem adantllr 481
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
Hypothesis
Ref Expression
adantl2.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
adantllr ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem adantllr
StepHypRef Expression
1 simpl 109 . 2 ((𝜑𝜏) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 402 1 ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
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:  ad4ant13  513  ad4ant134  1217  r19.29an  2619  diffifi  6896  fimax2gtrilemstep  6902  cnegexlem3  8136  cnegex  8137  lemul12b  8820  climshftlemg  11312  prodeq2  11567  fprodmodd  11651  lcmdvds  12081  pw2dvdslemn  12167  dfgrp3mlem  12973  tgcl  13649  metss  14079  ivthinclemlr  14200  ivthinclemur  14202
  Copyright terms: Public domain W3C validator