Theorem jctild 527

Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

Ref	Expression
jctild.1	⊢ (𝜑 → (𝜓 → 𝜒))
jctild.2	⊢ (𝜑 → 𝜃)

Assertion

Ref	Expression
jctild	⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Proof of Theorem jctild

Step	Hyp	Ref	Expression
1		jctild.2	. . 3 ⊢ (𝜑 → 𝜃)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 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:  anc2li  557  equvini  2455  2reu1  3892  frpoinsg  6345  ordunidif  6414  isofrlem  7337  dfwe2  7761  orduniorsuc  7818  tfisg  7843  poxp  8114  fnse  8119  ssenen  9151  dffi3  9426  fpwwe2lem12  10637  zmulcl  12611  rpneg  13006  rexuz3  15295  cau3lem  15301  climrlim2  15491  o1rlimmul  15563  iseralt  15631  gcdzeq  16494  isprm3  16620  vdwnnlem2  16929  ablfaclem3  19957  epttop  22512  lmcnp  22808  dfconn2  22923  txcnp  23124  cmphaushmeo  23304  isfild  23362  cnpflf2  23504  flimfnfcls  23532  alexsubALT  23555  fgcfil  24788  bcthlem5  24845  ivthlem2  24969  ivthlem3  24970  dvfsumrlim  25548  plypf1  25726  noetalem1  27244  n0sind  27706  axeuclidlem  28251  usgr2wlkneq  29044  wwlksnredwwlkn0  29181  wwlksnextwrd  29182  clwlkclwwlklem2a1  29276  lnon0  30082  hstles  31515  mdsl1i  31605  atcveq0  31632  atcvat4i  31681  cdjreui  31716  issgon  33152  connpconn  34257  outsideofrflx  35130  isbasisrelowllem1  36284  isbasisrelowllem2  36285  poimirlem3  36539  poimirlem29  36565  poimir  36569  heicant  36571  equivtotbnd  36694  ismtybndlem  36722  cvrat4  38362  linepsubN  38671  pmapsub  38687  osumcllem4N  38878  pexmidlem1N  38889  dochexmidlem1  40379  cantnfresb  42122  harval3  42337  clcnvlem  42422  iccpartimp  46133  sbgoldbwt  46493  sbgoldbst  46494  elsetrecslem  47792