Theorem jca2 518

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 517	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

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  3606  preddowncl  6283  ssimaex  6912  onfununi  8271  oaordex  8483  domtriord  9051  findcard3  9183  unfilem1  9205  fodomfibOLD  9231  inf0  9533  inf3lem3  9542  tcel  9655  fidomtri2  9909  alephval3  10023  zorn2lem6  10414  fodomb  10439  eqreznegel  12875  iserodd  16797  cshwsiun  17061  txcn  23609  ssfg  23855  fclsnei  24002  eldmgm  27003  fnrelpredd  35272  cvmlift2lem10  35540  axtco1from2  36703  bj-axreprepsep  37428  relcnveq3  38694  iss2  38711  elrelscnveq3  38994  jca3  39348  prjspreln0  43059  omabs2  43777  tfsconcatrn  43787  rfovcnvf1od  44448  mnuop3d  44715  ssclaxsep  45426