MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jca2 Structured version   Visualization version   GIF version

Theorem jca2 515
Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)
Hypotheses
Ref Expression
jca2.1 (𝜑 → (𝜓𝜒))
jca2.2 (𝜓𝜃)
Assertion
Ref Expression
jca2 (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem jca2
StepHypRef Expression
1 jca2.1 . 2 (𝜑 → (𝜓𝜒))
2 jca2.2 . . 3 (𝜓𝜃)
32a1i 11 . 2 (𝜑 → (𝜓𝜃))
41, 3jcad 514 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  rr19.28v  3624  preddowncl  6290  ssimaex  6930  onfununi  8291  oaordex  8509  domtriord  9073  findcard3  9235  findcard3OLD  9236  unfilem1  9260  fodomfib  9276  inf0  9565  inf3lem3  9574  tcel  9689  fidomtri2  9938  alephval3  10054  zorn2lem6  10445  fodomb  10470  eqreznegel  12867  iserodd  16715  cshwsiun  16980  txcn  23000  ssfg  23246  fclsnei  23393  eldmgm  26394  fnrelpredd  33757  cvmlift2lem10  33970  relcnveq3  36832  iss2  36855  elrelscnveq3  37003  jca3  37368  prjspreln0  40994  omabs2  41714  rfovcnvf1od  42368  mnuop3d  42643
  Copyright terms: Public domain W3C validator