Theorem jca2 513

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

Step	Hyp	Ref	Expression
1		jca2.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jca2.2	. . 3 ⊢ (𝜓 → 𝜃)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 512	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  rr19.28v  3624  preddowncl  6298  ssimaex  6927  onfununi  8283  oaordex  8495  domtriord  9063  findcard3  9195  unfilem1  9217  fodomfibOLD  9243  inf0  9542  inf3lem3  9551  tcel  9664  fidomtri2  9918  alephval3  10032  zorn2lem6  10423  fodomb  10448  eqreznegel  12859  iserodd  16775  cshwsiun  17039  txcn  23582  ssfg  23828  fclsnei  23975  eldmgm  27000  fnrelpredd  35266  cvmlift2lem10  35525  bj-axreprepsep  37320  relcnveq3  38575  iss2  38592  elrelscnveq3  38875  jca3  39229  prjspreln0  42964  omabs2  43686  tfsconcatrn  43696  rfovcnvf1od  44357  mnuop3d  44624  ssclaxsep  45335