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  3618  preddowncl  6284  ssimaex  6923  onfununi  8279  oaordex  8497  domtriord  9025  findcard3  9187  findcard3OLD  9188  unfilem1  9212  fodomfib  9228  inf0  9515  inf3lem3  9524  tcel  9639  fidomtri2  9888  alephval3  10004  zorn2lem6  10395  fodomb  10420  eqreznegel  12813  iserodd  16661  cshwsiun  16926  txcn  22923  ssfg  23169  fclsnei  23316  eldmgm  26317  fnrelpredd  33521  cvmlift2lem10  33734  relcnveq3  36714  iss2  36737  elrelscnveq3  36885  jca3  37250  prjspreln0  40850  omabs2  41566  rfovcnvf1od  42181  mnuop3d  42456
  Copyright terms: Public domain W3C validator