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  3668  preddowncl  6353  ssimaex  6994  onfununi  8381  oaordex  8596  domtriord  9163  findcard3  9318  findcard3OLD  9319  unfilem1  9343  fodomfibOLD  9371  inf0  9661  inf3lem3  9670  tcel  9785  fidomtri2  10034  alephval3  10150  zorn2lem6  10541  fodomb  10566  eqreznegel  12976  iserodd  16873  cshwsiun  17137  txcn  23634  ssfg  23880  fclsnei  24027  eldmgm  27065  fnrelpredd  35103  cvmlift2lem10  35317  relcnveq3  38322  iss2  38345  elrelscnveq3  38492  jca3  38857  prjspreln0  42619  omabs2  43345  tfsconcatrn  43355  rfovcnvf1od  44017  mnuop3d  44290  ssclaxsep  44999