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

Theorem jca2 512
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 511 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  rr19.28v  3655  preddowncl  6345  ssimaex  6987  onfununi  8371  oaordex  8588  domtriord  9161  findcard3  9319  findcard3OLD  9320  unfilem1  9344  fodomfibOLD  9373  inf0  9664  inf3lem3  9673  tcel  9788  fidomtri2  10037  alephval3  10153  zorn2lem6  10544  fodomb  10569  eqreznegel  12970  iserodd  16837  cshwsiun  17102  txcn  23621  ssfg  23867  fclsnei  24014  eldmgm  27050  fnrelpredd  34926  cvmlift2lem10  35140  relcnveq3  38019  iss2  38042  elrelscnveq3  38189  jca3  38554  prjspreln0  42263  omabs2  42998  tfsconcatrn  43008  rfovcnvf1od  43671  mnuop3d  43945
  Copyright terms: Public domain W3C validator