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

Theorem jca2 514
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 513 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  rr19.28v  3623  preddowncl  6291  ssimaex  6931  onfununi  8292  oaordex  8510  domtriord  9074  findcard3  9236  findcard3OLD  9237  unfilem1  9261  fodomfib  9277  inf0  9566  inf3lem3  9575  tcel  9690  fidomtri2  9939  alephval3  10055  zorn2lem6  10446  fodomb  10471  eqreznegel  12868  iserodd  16718  cshwsiun  16983  txcn  23014  ssfg  23260  fclsnei  23407  eldmgm  26408  fnrelpredd  33782  cvmlift2lem10  33993  relcnveq3  36855  iss2  36878  elrelscnveq3  37026  jca3  37391  prjspreln0  41005  omabs2  41725  tfsconcatrn  41735  rfovcnvf1od  42398  mnuop3d  42673
  Copyright terms: Public domain W3C validator