Theorem expcomd 422

Description: Deduction form of expcom 419. (Contributed by Alan Sare, 22-Jul-2012.)

Hypothesis

Ref	Expression
expcomd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expcomd	⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Proof of Theorem expcomd

Step	Hyp	Ref	Expression
1		expcomd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 421	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 87	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ancomsd  471  simplbi2comt  507  ralrimdva  3162  reupick  4274  pwssun  5542  ordelord  6384  tz7.7  6388  onelssex  6412  poxp  8142  smores2  8365  smoiun  8372  smogt  8378  tz7.49  8458  omsmolem  8669  mapxpen  9165  fodomfir  9322  f1dmvrnfibi  9333  suplub2  9456  epfrs  9735  r1sdom  9784  rankr1ai  9809  hfelhfOLD  9919  ficardom  10045  cardsdomel  10058  dfac5lem5  10209  cfsmolem  10351  cfcoflem  10353  axdc3lem2  10532  zorn2lem7  10583  genpn0  11091  reclem2pr  11136  supsrlem  11199  ltletr  11405  fzind  12800  rpneg  13157  xrltletr  13289  iccid  13524  ssfzoulel  13898  ssfzo12bi  13899  pfxccatin12lem2  14884  swrdccat  14888  repsdf2  14933  repswswrd  14939  cshwcsh2id  14983  o1rlimmul  15791  dvdsabseq  16488  divalgb  16579  bezoutlem3  16719  cncongr1  16847  ncoprmlnprm  16909  difsqpwdvds  17070  lss1d  21243  pf1ind  22678  chfacfisf  23177  chfacfisfcpmat  23178  cayleyhamilton1  23215  txlm  23972  fmfnfmlem1  24278  blsscls2  24828  metcnpi3  24870  bcmono  27609  lestr  28124  elreno2  28886  upgrewlkle2  30192  redwlk  30256  crctcshwlkn0lem5  30408  wwlksnextwrd  30491  clwwlknonex2lem2  30704  ocnel  31905  atcvat2i  32994  atcvat4i  33004  rankfilimb  35780  trssfir1om  35789  trssfir1omregs  35860  dfon2lem5  36641  cgrxfr  36912  colinearxfr  36932  isbasisrelowllem1  38371  isbasisrelowllem2  38372  finxpreclem6  38412  seqpo  38774  atlatle  40470  cvrexchlem  40569  cvrat2  40579  cvrat4  40593  pmapjoin  41002  onfrALTlem2  45622  onfrALTlem2VD  45964  eluzge0nn0  48475  elfz2z  48478  iccpartiltu  48597  iccpartigtl  48598  iccpartlt  48599  lighneal  48789  bgoldbtbnd  49000  tgoldbach  49008  cznnring  49452  ply1mulgsumlem2  49592  itsclc0  49976