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

Theorem impancom 258
Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
Hypothesis
Ref Expression
impancom.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
impancom ((𝜑𝜒) → (𝜓𝜃))

Proof of Theorem impancom
StepHypRef Expression
1 impancom.1 . . . 4 ((𝜑𝜓) → (𝜒𝜃))
21ex 114 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 78 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
43imp 123 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  eqrdav  2099  disjiun  3870  euotd  4114  onsucelsucr  4362  isotr  5649  spc2ed  6060  ltbtwnnqq  7124  genpcdl  7228  genpcuu  7229  un0addcl  8862  un0mulcl  8863  btwnnz  8997  uznfz  9724  elfz0ubfz0  9743  fzoss1  9789  elfzo0z  9802  fzofzim  9806  elfzom1p1elfzo  9832  ssfzo12bi  9843  subfzo0  9860  modfzo0difsn  10009  expaddzap  10178  caucvgre  10593  caubnd2  10729  summodc  10991  fzo0dvdseq  11350  nno  11398  lcmdvds  11553  hashgcdeq  11696  neii1  12098  neii2  12100
  Copyright terms: Public domain W3C validator