Theorem jca2 515

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  rr19.28v  3659  preddowncl  6334  ssimaex  6977  onfununi  8341  oaordex  8558  domtriord  9123  findcard3  9285  findcard3OLD  9286  unfilem1  9310  fodomfib  9326  inf0  9616  inf3lem3  9625  tcel  9740  fidomtri2  9989  alephval3  10105  zorn2lem6  10496  fodomb  10521  eqreznegel  12918  iserodd  16768  cshwsiun  17033  txcn  23130  ssfg  23376  fclsnei  23523  eldmgm  26526  fnrelpredd  34092  cvmlift2lem10  34303  relcnveq3  37190  iss2  37213  elrelscnveq3  37361  jca3  37726  prjspreln0  41351  omabs2  42082  tfsconcatrn  42092  rfovcnvf1od  42755  mnuop3d  43030