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  3647  preddowncl  6321  ssimaex  6964  onfununi  8355  oaordex  8570  domtriord  9137  findcard3  9290  findcard3OLD  9291  unfilem1  9315  fodomfibOLD  9343  inf0  9635  inf3lem3  9644  tcel  9759  fidomtri2  10008  alephval3  10124  zorn2lem6  10515  fodomb  10540  eqreznegel  12950  iserodd  16855  cshwsiun  17119  txcn  23564  ssfg  23810  fclsnei  23957  eldmgm  26984  fnrelpredd  35120  cvmlift2lem10  35334  relcnveq3  38339  iss2  38362  elrelscnveq3  38509  jca3  38874  prjspreln0  42632  omabs2  43356  tfsconcatrn  43366  rfovcnvf1od  44028  mnuop3d  44295  ssclaxsep  45007