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 208  df-an 397
This theorem is referenced by:  rr19.28v  3665  preddowncl  6172  ssimaex  6744  onfununi  7972  oaordex  8177  domtriord  8655  findcard3  8753  unfilem1  8774  fodomfib  8790  inf0  9076  inf3lem3  9085  tcel  9179  fidomtri2  9415  alephval3  9528  zorn2lem6  9915  fodomb  9940  eqreznegel  12326  iserodd  16164  cshwsiun  16425  txcn  22152  ssfg  22398  fclsnei  22545  eldmgm  25515  cvmlift2lem10  32445  relcnveq3  35448  iss2  35471  elrelscnveq3  35600  jca3  35861  prjspreln0  39126  rfovcnvf1od  40217  mnuop3d  40474
  Copyright terms: Public domain W3C validator