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  3599  preddowncl  6235  ssimaex  6853  onfununi  8172  oaordex  8389  domtriord  8910  findcard3  9057  unfilem1  9078  fodomfib  9093  inf0  9379  inf3lem3  9388  tcel  9503  fidomtri2  9752  alephval3  9866  zorn2lem6  10257  fodomb  10282  eqreznegel  12674  iserodd  16536  cshwsiun  16801  txcn  22777  ssfg  23023  fclsnei  23170  eldmgm  26171  fnrelpredd  33061  cvmlift2lem10  33274  relcnveq3  36456  iss2  36479  elrelscnveq3  36609  jca3  36870  prjspreln0  40448  rfovcnvf1od  41612  mnuop3d  41889
  Copyright terms: Public domain W3C validator